$\forall$${\it the\_es}$:ES, $j$:E. $\neg$first($j$) $\Rightarrow$ pred($j$) $\leq$ $j$